var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https://autonomy-and-verification.github.io/pubs.bib&jsonp=1&group0=year&filter=note:RAIN|ORCA|FAIR-SPACE&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https://autonomy-and-verification.github.io/pubs.bib&jsonp=1&group0=year&filter=note:RAIN|ORCA|FAIR-SPACE\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https://autonomy-and-verification.github.io/pubs.bib&jsonp=1&group0=year&filter=note:RAIN|ORCA|FAIR-SPACE\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
    2. \n
  2. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
    3. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2023\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Adaptive Cognitive Agents: Updating Action Descriptions and Plans.\n \n \n \n\n\n \n Stringer, P.; Cardoso, R. C.; Dixon, C.; Fisher, M.; and Dennis, L. A.\n\n\n \n\n\n\n In Malvone, V.; and Murano, A., editor(s), Multi-Agent Systems, pages 345–362, Cham, 2023. Springer Nature Switzerland\n [RAIN, FAIR-Space,TAS Verifiability Node, Computational Agent Responsibility]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{10.1007/978-3-031-43264-4_22,\nauthor="Stringer, Peter\nand Cardoso, Rafael C.\nand Dixon, Clare\nand Fisher, Michael\nand Dennis, Louise A.",\neditor="Malvone, Vadim\nand Murano, Aniello",\ntitle="Adaptive Cognitive Agents: Updating Action Descriptions and Plans",\nbooktitle="Multi-Agent Systems",\nyear="2023",\npublisher="Springer Nature Switzerland",\naddress="Cham",\npages="345--362",\nabstract="In this paper we present an extension of Belief-Desire-Intention agents which can adapt their performance in response to changes in their environment. We consider situations in which the agent's actions no longer perform as anticipated. Our agents maintain explicit descriptions of the expected behaviour of their actions, are able to track action performance, learn new action descriptions and patch affected plans at runtime. Our main contributions are the underlying theoretical mechanisms for data collection about action performance, the synthesis of new action descriptions from this data and the integration with plan reconfiguration. The mechanisms are supported by a practical implementation to validate the approach.",\nisbn="978-3-031-43264-4",\nnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>,<span class="tas_vn">TAS Verifiability Node</span>, <span class="car">Computational Agent Responsibility</span>]}\n}\n
\n
\n\n\n
\n In this paper we present an extension of Belief-Desire-Intention agents which can adapt their performance in response to changes in their environment. We consider situations in which the agent's actions no longer perform as anticipated. Our agents maintain explicit descriptions of the expected behaviour of their actions, are able to track action performance, learn new action descriptions and patch affected plans at runtime. Our main contributions are the underlying theoretical mechanisms for data collection about action performance, the synthesis of new action descriptions from this data and the integration with plan reconfiguration. The mechanisms are supported by a practical implementation to validate the approach.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Autonomous Systems' Safety Cases for use in UK Nuclear Environments.\n \n \n \n \n\n\n \n Anderson, C. R.; and Dennis, L. A.\n\n\n \n\n\n\n Electronic Proceedings in Theoretical Computer Science, 391: 83–88. sep 2023.\n [RAIN]\n\n\n\n
\n\n\n\n \n \n \"AutonomousPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{Anderson_2023,\n\tdoi = {10.4204/eptcs.391.10},  \n\turl = {https://doi.org/10.4204%2Feptcs.391.10},\n\tyear = 2023,\n\tmonth = {sep},\n\tpublisher = {Open Publishing Association},\n\tvolume = {391},\n\tpages = {83--88},\n\tauthor = {Christopher R. Anderson and Louise A. Dennis},\n\ttitle = {Autonomous Systems{\\textquotesingle} Safety Cases for use in {UK} Nuclear Environments},\n\tjournal = {Electronic Proceedings in Theoretical Computer Science},\n\tnote={[<span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verifiable Autonomous Systems: Using Rational Agents to Provide Assurance about Decisions Made by Machines.\n \n \n \n\n\n \n Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n Cambridge University Press, 2023.\n [RAIN, FAIR-Space,TAS Verifiability Node,Verifiable Autonomy,RAEng]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{dennisfisher23,\nauthor={Louise A. Dennis and Michael Fisher},\ntitle={Verifiable Autonomous Systems: Using Rational Agents to Provide Assurance about Decisions Made by Machines},\npublisher={Cambridge University Press},\nyear={2023},\nnote = {[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>,<span class="tas_vn">TAS Verifiability Node</span>,<span class="va">Verifiable Autonomy</span>,<span class="raeng">RAEng</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Updating Action Descriptions and Plans for Cognitive Agents.\n \n \n \n\n\n \n Stringer, P.; Cardoso, R. C.; Dixon, C.; Fisher, M.; and Dennis, L. A.\n\n\n \n\n\n\n In Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems, of AAMAS '23, pages 2370–2372, Richland, SC, 2023. International Foundation for Autonomous Agents and Multiagent Systems\n [RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@inproceedings{stringer23, \nauthor = {Stringer, Peter and Cardoso, Rafael C. and Dixon, Clare and Fisher, Michael and Dennis, Louise A.}, \ntitle = {Updating Action Descriptions and Plans for Cognitive Agents}, year = {2023}, isbn = {9781450394321}, \npublisher = {International Foundation for Autonomous Agents and Multiagent Systems}, \naddress = {Richland, SC}, \nbooktitle = {Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems}, \npages = {2370–2372}, numpages = {3}, \nkeywords = {action descriptions, ai planning, beliefs-desires-intentions}, location = {London, United Kingdom}, series = {AAMAS '23} ,\nnote = {[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Should AI Systems in Nuclear Facilities Explain Decisions the Way Humans Do? An Interview Study.\n \n \n \n\n\n \n Taylor, H. M; Jay, C.; Lennox, B.; Cangelosi, A.; and Dennis, L.\n\n\n \n\n\n\n In 2022 31st IEEE International Conference on Robot and Human Interactive Communication (RO-MAN), pages 956-962, 2022. \n [RAIN]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@INPROCEEDINGS{9900852,\n  author={Taylor, Hazel M and Jay, Caroline and Lennox, Barry and Cangelosi, Angelo and Dennis, Louise},\n  booktitle={2022 31st IEEE International Conference on Robot and Human Interactive Communication (RO-MAN)},\n  title={Should AI Systems in Nuclear Facilities Explain Decisions the Way Humans Do? An Interview Study},\n  year={2022},\n  volume={},\n  number={},\n  pages={956-962},\n  doi={10.1109/RO-MAN53752.2022.9900852},\n  note = {[<span class="rain">RAIN</span>]}\n  }\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verifying Autonomous Systems.\n \n \n \n\n\n \n Dennis, L. A.\n\n\n \n\n\n\n In ter Beek, M. H.; and Monahan, R., editor(s), Integrated Formal Methods, pages 3–17, Cham, 2022. Springer International Publishing\n [RAIN, FAIR-Space, TAS Verifiability Node, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{IFM_Keynote,\nauthor="Dennis, Louise A.",\neditor="ter Beek, Maurice H.\nand Monahan, Rosemary",\ntitle="Verifying Autonomous Systems",\nbooktitle="Integrated Formal Methods",\nyear="2022",\npublisher="Springer International Publishing",\naddress="Cham",\npages="3--17",\nabstract="This paper focuses on the work of the Autonomy and Verification Network (https://autonomy-and-verification.github.io). In particular it will look at the use of model-checking to verify the choices made by a cognitive agent in control of decision making within an autonomous system. It will consider the assumptions that need to be made about the environment in which the agent operates in order to perform that verification and how those assumptions can be validated via runtime monitoring. Lastly it will consider how compositional techniques can be used to combine the agent verification with verification of other components within the autonomous system.",\nisbn="978-3-031-07727-2",\ndoi="10.1007/978-3-031-07727-2_1",\nnote = {[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="tas_vn">TAS Verifiability Node</span>, <span  class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n
\n This paper focuses on the work of the Autonomy and Verification Network (https://autonomy-and-verification.github.io). In particular it will look at the use of model-checking to verify the choices made by a cognitive agent in control of decision making within an autonomous system. It will consider the assumptions that need to be made about the environment in which the agent operates in order to perform that verification and how those assumptions can be validated via runtime monitoring. Lastly it will consider how compositional techniques can be used to combine the agent verification with verification of other components within the autonomous system.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Explaining BDI Agent Behaviour through Dialogue.\n \n \n \n\n\n \n Dennis, L. A.; and Oren, N.\n\n\n \n\n\n\n Journal of Autonomous Agents and Multi-Agent Systems. 2022.\n [RAIN, FAIR-Space, TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{DennisOren22,\n      author = {Louise A. Dennis and Nir Oren},\n      title = {Explaining {BDI} Agent Behaviour through Dialogue},\n      journal = {Journal of Autonomous Agents and Multi-Agent Systems},\n      year = 2022,\n      doi={10.1007/s10458-022-09556-8},\n      note = {[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="tas_vn">TAS Verifiability Node</span>]}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Implementing Durative Actions with Failure Detection in Gwendolen.\n \n \n \n\n\n \n Stringer, P.; Cardoso, R. C.; Dixon, C.; and Dennis, L. A.\n\n\n \n\n\n\n In Alechina, N.; Baldoni, M.; and Logan, B., editor(s), 9th International Workshop on Engineering Multi-Agent Systems, pages 332–351, Cham, 2022. Springer International Publishing\n [RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Stringer21a,\n      author={Peter Stringer and Rafael C. Cardoso and Clare Dixon and Louise A. Dennis},\n      title={Implementing Durative Actions with Failure Detection in Gwendolen},\n      booktitle={9th International Workshop on Engineering Multi-Agent Systems},\n      year={2022},\n      editor={Alechina, Natasha\nand Baldoni, Matteo\nand Logan, Brian},\npublisher={Springer International Publishing},\naddress={Cham},\npages={332--351},\n      note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n      }\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (18)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Principles for the Development and Assurance of Autonomous Systems for Safe Use in Hazardous Environments.\n \n \n \n \n\n\n \n Luckcuck, M.; Fisher, M.; Dennis, L.; Frost, S.; White, A.; and Styles, D.\n\n\n \n\n\n\n Technical Report Zenodo, June 2021.\n [RAIN]\n\n\n\n
\n\n\n\n \n \n \"PrinciplesPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@techreport{principles_white_paper_2021,\n\ttitle = {Principles for the {Development} and {Assurance} of {Autonomous} {Systems} for {Safe} {Use} in {Hazardous} {Environments}},\n\tcopyright = {Creative Commons Attribution 4.0 International, Open Access},\n\turl = {https://zenodo.org/record/5012322},\n\tabstract = {Autonomous systems are increasingly being used (or proposed for use) in situations where they are near or interact (physically or otherwise) with humans. They can be useful for performing tasks that are dirty or dangerous, or jobs that are simply distant or dull. This white paper sets out principles to consider when designing, developing, and regulating autonomous systems that are required to operate in hazardous environments. Autonomous systems use software to make decisions without the need for human control. They are often embedded in a robotic system, to enable interaction with the real world. This means that autonomous robotic systems are often safety-critical, where failures can cause human harm or death. For the sorts of autonomous robotic systems considered by this white paper, the risk of harm is likely to fall on human workers (the system’s users or operators). Autonomous systems also raise ssues of security and data privacy, both because of the sensitive data that the system might process and because a security failure can cause a safety failure. {\\textless}strong{\\textgreater}Scope{\\textless}/strong{\\textgreater} This white paper is intended to be an add-on to the relevant existing standards and guidance for (for example) robotics, electronic systems, control systems, and safety-critical software. These existing standards provide good practice for their respective areas, but do not provide guidance for autonomous systems. This white paper adds to the emerging good practice for developing autonomous robotic systems that are amenable to strong Verification \\&amp; Validation. The intended audience of this white paper is developers of autonomous and robotic systems. It aims to provide a description of things that need to be demonstrable by or of their systems, and recommendations of ways to achieve this. This aims to enable strong Verification \\&amp; Validation of the resulting autonomous system, and to mitigate some of the hazards already occurring in autonomous systems. {\\textless}strong{\\textgreater}Acknowledgments{\\textless}/strong{\\textgreater} Our thanks go to Vince Page, and Xiaowei Huang for contributing their expert advice; and to our early reviewers: Xingyu Zhao, Başak Sarac̣ -Lesavre, and Nick Hawes for their invaluable discussion and comments.},\n\tlanguage = {en},\n\turldate = {2021-08-30},\n\tinstitution = {Zenodo},\n\tauthor = {Luckcuck, Matt and Fisher, Michael and Dennis, Louise and Frost, Steve and White, Andy and Styles, Doug},\n\tmonth = jun,\n\tyear = {2021},\n\tdoi = {10.5281/ZENODO.5012322},\n\tkeywords = {Robotics, Validation, Verification, Autonomous Systems, Assurance, Hazardous Environments},\n\tannote = {Other\nThis white paper was written as part of the Robotics and AI in Nuclear (RAIN) project and is also available on the RAIN website: https://rainhub.org.uk/principles-for-the-development-and-assurance-of-autonomous-systems-for-safe-use-in-hazardous-environments-white-paper-published/},\nnote={[<span class="rain">RAIN</span>]}\n}\n\n\n\n
\n
\n\n\n
\n Autonomous systems are increasingly being used (or proposed for use) in situations where they are near or interact (physically or otherwise) with humans. They can be useful for performing tasks that are dirty or dangerous, or jobs that are simply distant or dull. This white paper sets out principles to consider when designing, developing, and regulating autonomous systems that are required to operate in hazardous environments. Autonomous systems use software to make decisions without the need for human control. They are often embedded in a robotic system, to enable interaction with the real world. This means that autonomous robotic systems are often safety-critical, where failures can cause human harm or death. For the sorts of autonomous robotic systems considered by this white paper, the risk of harm is likely to fall on human workers (the system’s users or operators). Autonomous systems also raise ssues of security and data privacy, both because of the sensitive data that the system might process and because a security failure can cause a safety failure. \\textlessstrong\\textgreaterScope\\textless/strong\\textgreater This white paper is intended to be an add-on to the relevant existing standards and guidance for (for example) robotics, electronic systems, control systems, and safety-critical software. These existing standards provide good practice for their respective areas, but do not provide guidance for autonomous systems. This white paper adds to the emerging good practice for developing autonomous robotic systems that are amenable to strong Verification & Validation. The intended audience of this white paper is developers of autonomous and robotic systems. It aims to provide a description of things that need to be demonstrable by or of their systems, and recommendations of ways to achieve this. This aims to enable strong Verification & Validation of the resulting autonomous system, and to mitigate some of the hazards already occurring in autonomous systems. \\textlessstrong\\textgreaterAcknowledgments\\textless/strong\\textgreater Our thanks go to Vince Page, and Xiaowei Huang for contributing their expert advice; and to our early reviewers: Xingyu Zhao, Başak Sarac̣ -Lesavre, and Nick Hawes for their invaluable discussion and comments.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; Papacchini, F.; Luckcuck, M.; Linker, S.; and Payne, T. R.\n\n\n \n\n\n\n In Ahlbrecht, T.; Dix, J.; Fiekas, N.; and Krausburg, T., editor(s), The Multi-Agent Programming Contest 2021, pages 82–107, Cham, 2021. Springer International Publishing\n [RAEng, RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{Cardoso21f,\nauthor="Cardoso, Rafael C.\nand Ferrando, Angelo\nand Papacchini, Fabio\nand Luckcuck, Matt\nand Linker, Sven\nand Payne, Terry R.",\neditor="Ahlbrecht, Tobias\nand Dix, J{\\"u}rgen\nand Fiekas, Niklas\nand Krausburg, Tabajara",\ntitle="MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest",\nbooktitle="The Multi-Agent Programming Contest 2021",\nyear="2021",\npublisher="Springer International Publishing",\naddress="Cham",\npages="82--107",\nabstract="In this paper, we describe the strategies used by our team, MLFC, that led us to achieve the 2nd place in the 15th edition of the Multi-Agent Programming Contest. The scenario used in the contest is an extension of the previous edition (14th) ``Agents Assemble'' wherein two teams of agents move around a 2D grid and compete to assemble complex block structures. We discuss the languages and tools used during the development of our team. Then, we summarise the main strategies that were carried over from our previous participation in the 14th edition and list the limitations (if any) of using these strategies in the latest contest edition. We also developed new strategies that were made specifically for the extended scenario: cartography (determining the size of the map); formal verification of the map merging protocol (to provide assurances that it works when increasing the number of agents); plan cache (efficiently scaling the number of planners); task achievement (forming groups of agents to achieve tasks); and bullies (agents that focus on stopping agents from the opposing team). Finally, we give a brief overview of our performance in the contest and discuss what we believe were our shortcomings.",\nisbn="978-3-030-88549-6",\ndoi="10.1007/978-3-030-88549-6_4",\nnote={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n}\n\n
\n
\n\n\n
\n In this paper, we describe the strategies used by our team, MLFC, that led us to achieve the 2nd place in the 15th edition of the Multi-Agent Programming Contest. The scenario used in the contest is an extension of the previous edition (14th) ``Agents Assemble'' wherein two teams of agents move around a 2D grid and compete to assemble complex block structures. We discuss the languages and tools used during the development of our team. Then, we summarise the main strategies that were carried over from our previous participation in the 14th edition and list the limitations (if any) of using these strategies in the latest contest edition. We also developed new strategies that were made specifically for the extended scenario: cartography (determining the size of the map); formal verification of the map merging protocol (to provide assurances that it works when increasing the number of agents); plan cache (efficiently scaling the number of planners); task achievement (forming groups of agents to achieve tasks); and bullies (agents that focus on stopping agents from the opposing team). Finally, we give a brief overview of our performance in the contest and discuss what we believe were our shortcomings.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Use and Usability of Software Verification Methods to Detect Behaviour Interference when Teaching an Assistive Home Companion Robot: A proof-of-concept study.\n \n \n \n \n\n\n \n Koay, K. L.; Webster, M.; Dixon, C.; Gainer, P.; Syrdal, D.; Fisher, M.; and Dautenhahn, K.\n\n\n \n\n\n\n Paladyn, Journal of Behavioral Robotics, 12(1): 402–422. 2021.\n [RAEng, RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n \n \"UsePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{TeachMe21,\nauthor = {Kheng Lee Koay and Matt Webster and Clare Dixon and Paul Gainer and Dag Syrdal and Michael Fisher and Kerstin Dautenhahn},\ndoi = {doi:10.1515/pjbr-2021-0028},\nurl = {https://www.degruyter.com/document/doi/10.1515/pjbr-2021-0028/html},\ntitle = "{Use and Usability of Software Verification Methods to Detect Behaviour Interference when Teaching an Assistive Home Companion Robot: A proof-of-concept study}",\njournal = {Paladyn, Journal of Behavioral Robotics},\nnumber = {1},\nvolume = {12},\nyear = {2021},\npages = {402--422},\nnote={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Towards the Determination of Safe Operating Envelopes for Autonomous UAS in Offshore Inspection Missions.\n \n \n \n \n\n\n \n Page, V.; Dadswell, C.; Webster, M.; Jump, M.; and Fisher, M.\n\n\n \n\n\n\n Robotics, 10(3). 2021.\n [ORCA]\n\n\n\n
\n\n\n\n \n \n \"TowardsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@Article{PDWJF21,\nAUTHOR = {Page, Vincent and Dadswell, Christopher and Webster, Matt and Jump, Mike and Fisher, Michael},\nTITLE = "{Towards the Determination of Safe Operating Envelopes for Autonomous UAS in Offshore Inspection Missions}",\nJOURNAL = {Robotics},\nVOLUME = {10},\nYEAR = {2021},\nNUMBER = {3},\nARTICLE-NUMBER = {97},\nURL = {https://www.mdpi.com/2218-6581/10/3/97},\nISSN = {2218-6581},\nABSTRACT = {A drive to reduce costs, carbon emissions, and the number of required personnel in the offshore energy industry has led to proposals for the increased use of autonomous/robotic systems for many maintenance tasks. There are questions over how such missions can be shown to be safe. A corollary exists in the manned aviation world for helicopter–ship operations where a test pilot attempts to operate from a ship under a range of wind conditions and provides subjective feedback on the level of difficulty encountered. This defines the ship–helicopter operating limit envelope (SHOL). Due to the cost of creating a SHOL there has been considerable research activity to demonstrate that much of this process can be performed virtually. Unmanned vehicles, however, have no test pilot to provide feedback. This paper therefore explores the possibility of adapting manned simulation techniques to the unmanned world to demonstrate that a mission is safe. Through flight modelling and simulation techniques it is shown that operating envelopes can be created for an oil rig inspection task and that, by using variable performance specifications, these can be tailored to suit the level of acceptable risk. The operating envelopes produced provide condensed and intelligible information regarding the environmental conditions under which the UAS can perform the task.},\nDOI = {10.3390/robotics10030097},\nnote={[<span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n
\n A drive to reduce costs, carbon emissions, and the number of required personnel in the offshore energy industry has led to proposals for the increased use of autonomous/robotic systems for many maintenance tasks. There are questions over how such missions can be shown to be safe. A corollary exists in the manned aviation world for helicopter–ship operations where a test pilot attempts to operate from a ship under a range of wind conditions and provides subjective feedback on the level of difficulty encountered. This defines the ship–helicopter operating limit envelope (SHOL). Due to the cost of creating a SHOL there has been considerable research activity to demonstrate that much of this process can be performed virtually. Unmanned vehicles, however, have no test pilot to provide feedback. This paper therefore explores the possibility of adapting manned simulation techniques to the unmanned world to demonstrate that a mission is safe. Through flight modelling and simulation techniques it is shown that operating envelopes can be created for an oil rig inspection task and that, by using variable performance specifications, these can be tailored to suit the level of acceptable risk. The operating envelopes produced provide condensed and intelligible information regarding the environmental conditions under which the UAS can perform the task.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Using formal methods for autonomous systems: Five recipes for formal verification.\n \n \n \n \n\n\n \n Luckcuck, M.\n\n\n \n\n\n\n Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability, 0(0): 1748006X211034970. 2021.\n [RAIN]\n\n\n\n
\n\n\n\n \n \n \"UsingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{luckcuck_using_2021,\nauthor = {Matt Luckcuck},\ntitle ={Using formal methods for autonomous systems: Five recipes for formal verification},\njournal = {Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability},\nvolume = {0},\nnumber = {0},\npages = {1748006X211034970},\nyear = {2021},\ndoi = {10.1177/1748006X211034970},\nURL = { https://doi.org/10.1177/1748006X211034970},\neprint = { https://doi.org/10.1177/1748006X211034970 },\nnote={[<span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Agile Tasking of Robotic Kitting.\n \n \n \n\n\n \n Michaloski, J.; Aksu, M.; Schlenoff, C.; Cardoso, R. C.; and Fisher, M.\n\n\n \n\n\n\n In Proceedings of the ASME 2021 International Mechanical Engineering Congress and Exposition (IMECE2021), 2021. \n [RAEng, RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{JohnIMECE,\n  title={Agile Tasking of Robotic Kitting},\n  author={Michaloski, John and Aksu, Murat and Schlenoff, Craig and Cardoso, Rafael C. and Fisher, Michael},\n  booktitle={Proceedings of the ASME 2021 International Mechanical Engineering Congress and Exposition (IMECE2021)},\n  year={2021},\n  note={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Automated Planning and BDI Agents: A Case Study.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; and Papacchini, F.\n\n\n \n\n\n\n In Dignum, F.; Corchado, J. M.; and De La Prieta, F., editor(s), Advances in Practical Applications of Agents, Multi-Agent Systems, and Social Good. The PAAMS Collection, pages 52–63, Cham, 2021. Springer International Publishing\n [RAEng, RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Cardoso21e,\n\tauthor="Cardoso, Rafael C.\n\tand Ferrando, Angelo\n\tand Papacchini, Fabio",\n\teditor="Dignum, Frank\n\tand Corchado, Juan Manuel\n\tand De La Prieta, Fernando",\n\ttitle="Automated Planning and BDI Agents: A Case Study",\n\tbooktitle="Advances in Practical Applications of Agents, Multi-Agent Systems, and Social Good. The PAAMS Collection",\n\tyear="2021",\n\tpublisher="Springer International Publishing",\n\taddress="Cham",\n\tpages="52--63",\n\tabstract="There have been many attempts to integrate automated planning and rational agents. Most of the research focuses on adding support directly within agent programming languages, such as those based on the Belief-Desire-Intention model, rather than using off-the-shelf planners. This approach is often believed to improve the computation time, which is a common requirement in real world applications. This paper shows that even in complex scenarios, such as in the Multi-Agent Programming Contest with 50 agents and a 4 s deadline for the agents to send actions to the server, it is possible to efficiently integrate agent languages with off-the-shelf automated planners. Based on the experience with this case study, the paper discusses advantages and disadvantages of decoupling the agents from the planners.",\n\tisbn="978-3-030-85739-4",\n\tdoi={10.1007/978-3-030-85739-4_5},\n\tnote={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n}\n\n
\n
\n\n\n
\n There have been many attempts to integrate automated planning and rational agents. Most of the research focuses on adding support directly within agent programming languages, such as those based on the Belief-Desire-Intention model, rather than using off-the-shelf planners. This approach is often believed to improve the computation time, which is a common requirement in real world applications. This paper shows that even in complex scenarios, such as in the Multi-Agent Programming Contest with 50 agents and a 4 s deadline for the agents to send actions to the server, it is possible to efficiently integrate agent languages with off-the-shelf automated planners. Based on the experience with this case study, the paper discusses advantages and disadvantages of decoupling the agents from the planners.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n RVPLAN: A General Purpose Framework for Replanning using Runtime Verification.\n \n \n \n\n\n \n Ferrando, A.; and Cardoso, R. C.\n\n\n \n\n\n\n In Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21), 2021. \n [RAEng, RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{FerrandoVortex,\n  title={RVPLAN: A General Purpose Framework for Replanning using Runtime Verification},\n  author={Ferrando, Angelo and Cardoso, Rafael C.},\n  booktitle={Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21)},\n  year={2021},\n  note={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Increasing Confidence in Autonomous Systems.\n \n \n \n\n\n \n Fisher, M.; Ferrando, A.; and Cardoso, R. C.\n\n\n \n\n\n\n In Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21), 2021. \n [RAEng, RAIN, FAIR-Space, ORCA, TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{fisher2021increasing,\n  title={Increasing Confidence in Autonomous Systems},\n  author={Fisher, Michael and Ferrando, Angelo and Cardoso, Rafael C.},\n  booktitle={Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21)},\n  year={2021},\n  note={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>, <span class="tas_vn">TAS Verifiability Node</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Agents and Robots for Reliable Engineered Autonomy:A Perspective from the Organisers of AREA 2020.\n \n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; Briola, D.; Menghi, C.; and Ahlbrecht, T.\n\n\n \n\n\n\n Journal of Sensor and Actuator Networks, 10(2). 2021.\n [RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n \n \"AgentsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{cardoso21e,\nAUTHOR = {Cardoso, Rafael C. and Ferrando, Angelo and Briola, Daniela and Menghi, Claudio and Ahlbrecht, Tobias},\nTITLE = {Agents and Robots for Reliable Engineered Autonomy:A Perspective from the Organisers of AREA 2020},\nJOURNAL = {Journal of Sensor and Actuator Networks},\nVOLUME = {10},\nYEAR = {2021},\nNUMBER = {2},\nARTICLE-NUMBER = {33},\nURL = {https://www.mdpi.com/2224-2708/10/2/33},\nISSN = {2224-2708},\nABSTRACT = {Multi-agent systems, robotics and software engineering are large and active research areas with many applications in academia and industry. The First Workshop on Agents and Robots for reliable Engineered Autonomy (AREA), organised the first time in 2020, aims at encouraging cross-disciplinary collaborations and exchange of ideas among researchers working in these research areas. This paper presents a perspective of the organisers that aims at highlighting the latest research trends, future directions, challenges, and open problems. It also includes feedback from the discussions held during the AREA workshop. The goal of this perspective is to provide a high-level view of current research trends for researchers that aim at working in the intersection of these research areas.},\nDOI = {10.3390/jsan10020033},\nnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n
\n Multi-agent systems, robotics and software engineering are large and active research areas with many applications in academia and industry. The First Workshop on Agents and Robots for reliable Engineered Autonomy (AREA), organised the first time in 2020, aims at encouraging cross-disciplinary collaborations and exchange of ideas among researchers working in these research areas. This paper presents a perspective of the organisers that aims at highlighting the latest research trends, future directions, challenges, and open problems. It also includes feedback from the discussions held during the AREA workshop. The goal of this perspective is to provide a high-level view of current research trends for researchers that aim at working in the intersection of these research areas.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n An Overview of Verification and Validation Challenges for Inspection Robots.\n \n \n \n \n\n\n \n Fisher, M.; Cardoso, R. C.; Collins, E. C.; Dadswell, C.; Dennis, L. A.; Dixon, C.; Farrell, M.; Ferrando, A.; Huang, X.; Jump, M.; Kourtis, G.; Lisitsa, A.; Luckcuck, M.; Luo, S.; Page, V.; Papacchini, F.; and Webster, M.\n\n\n \n\n\n\n Robotics, 10(2). 2021.\n [RAIN, FAIR-Space, ORCA, RAEng]\n\n\n\n
\n\n\n\n \n \n \"AnPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{robotics10020067,\nauthor = {Fisher, Michael and Cardoso, Rafael C. and Collins, Emily C. and Dadswell, Christopher and Dennis, Louise A. and Dixon, Clare and Farrell, Marie and Ferrando, Angelo and Huang, Xiaowei and Jump, Mike and Kourtis, Georgios and Lisitsa, Alexei and Luckcuck, Matt and Luo, Shan and Page, Vincent and Papacchini, Fabio and Webster, Matt},\ntitle = {An Overview of Verification and Validation Challenges for Inspection Robots},\njournal = {Robotics},\nvolume = {10},\nyear = {2021},\nnumber = {2},\nurl = {https://www.mdpi.com/2218-6581/10/2/67},\nissn = {2218-6581},\nabstract = {The advent of sophisticated robotics and AI technology makes sending humans into hazardous and distant environments to carry out inspections increasingly avoidable. Being able to send a robot, rather than a human, into a nuclear facility or deep space is very appealing. However, building these robotic systems is just the start and we still need to carry out a range of verification and validation tasks to ensure that the systems to be deployed are as safe and reliable as possible. Based on our experience across three research and innovation hubs within the UK’s “Robots for a Safer World” programme, we present an overview of the relevant techniques and challenges in this area. As the hubs are active across nuclear, offshore, and space environments, this gives a breadth of issues common to many inspection robots.},\ndoi = {10.3390/robotics10020067},\nnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>, <span class="raeng">RAEng</span>]}\n}\n\n
\n
\n\n\n
\n The advent of sophisticated robotics and AI technology makes sending humans into hazardous and distant environments to carry out inspections increasingly avoidable. Being able to send a robot, rather than a human, into a nuclear facility or deep space is very appealing. However, building these robotic systems is just the start and we still need to carry out a range of verification and validation tasks to ensure that the systems to be deployed are as safe and reliable as possible. Based on our experience across three research and innovation hubs within the UK’s “Robots for a Safer World” programme, we present an overview of the relevant techniques and challenges in this area. As the hubs are active across nuclear, offshore, and space environments, this gives a breadth of issues common to many inspection robots.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Formal Verification of a Map Merging Protocol in the Multi-Agent Programming Contest.\n \n \n \n\n\n \n Luckcuck, M.; and Cardoso, R. C.\n\n\n \n\n\n\n In 9th International Workshop on Engineering Multi-Agent Systems, 2021. \n [RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Luckcuck21a,\n      author={Matt Luckcuck and Rafael C. Cardoso},\n      title={Formal Verification of a Map Merging Protocol in the Multi-Agent Programming Contest},\n      booktitle={9th International Workshop on Engineering Multi-Agent Systems},\n      year={2021},\n      note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n      }\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Implementing Ethical Governors in BDI.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In 9th International Workshop on Engineering Multi-Agent Systems, 2021. \n [RAIN, FAIR-Space, ORCA, TAS Verifiability Node, RAEng]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Cardoso21c,\n      author={Rafael C. Cardoso and Angelo Ferrando and Louise A. Dennis and Michael Fisher},\n      title={Implementing Ethical Governors in BDI},\n      booktitle={9th International Workshop on Engineering Multi-Agent Systems},\n      year={2021},\n      note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>, <span class="tas_vn">TAS Verifiability Node</span>, <span class="raeng">RAEng</span>]}\n      }\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Agile Tasking of Robotic Systems with Explicit Autonomy.\n \n \n \n\n\n \n Cardoso, R. C.; Michaloski, J. L.; Schlenoff, C.; Ferrando, A.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In The International FLAIRS Conference Proceedings, volume 34, 2021. \n [RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{Cardoso21b,\ntitle={Agile Tasking of Robotic Systems with Explicit Autonomy},\nvolume={34},\nDOI={10.32473/flairs.v34i1.128481},\nbooktitle={The International FLAIRS Conference Proceedings},\nauthor={Cardoso, Rafael C. and Michaloski, John L. and Schlenoff, Craig and Ferrando, Angelo and Dennis, Louise A. and Fisher, Michael},\nyear={2021},\nnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Review of Agent-Based Programming for Multi-Agent Systems.\n \n \n \n\n\n \n Cardoso, R. C.; and Ferrando, A.\n\n\n \n\n\n\n Computers, 10(2): 16. Jan 2021.\n [RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 16 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{Cardoso21a,\ntitle={A Review of Agent-Based Programming for Multi-Agent Systems},\nvolume={10},\nISSN={2073-431X},\nDOI={10.3390/computers10020016},\nnumber={2},\njournal={Computers},\npublisher={MDPI AG},\nauthor={Cardoso, Rafael C. and Ferrando, Angelo},\nyear={2021},\nmonth={Jan},\npages={16},\nnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems.\n \n \n \n \n\n\n \n Ferrando, A.; Dennis, L. A.; Cardoso, R. C.; Fisher, M.; Ancona, D.; and Mascardi, V.\n\n\n \n\n\n\n ACM Trans. Softw. Eng. Methodol., 30(4). May 2021.\n [RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n \n \"TowardPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@article{Ferrando21,\n\tauthor = {Ferrando, Angelo and Dennis, Louise A. and Cardoso, Rafael C. and Fisher, Michael and Ancona, Davide and Mascardi, Viviana},\n\ttitle = {Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems},\n\tyear = {2021},\n\tissue_date = {May 2021},\n\tpublisher = {Association for Computing Machinery},\n\taddress = {New York, NY, USA},\n\tvolume = {30},\n\tnumber = {4},\n\tissn = {1049-331X},\n\turl = {https://doi.org/10.1145/3447246},\n\tdoi = {10.1145/3447246},\n\tabstract = {When applying formal verification to a system that interacts with the real world, we must use a model of the environment. This model represents an abstraction of the actual environment, so it is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well behaved. A solution to this problem consists in exploiting the model of the environment used for statically verifying the system’s behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The article discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies: an autonomous cruise control system and a simulation of the Mars Curiosity rover.},\n\tjournal = {ACM Trans. Softw. Eng. Methodol.},\n\tmonth = may,\n\tarticleno = {43},\n\tnumpages = {43},\n\tkeywords = {autonomous systems, model checking, trace expressions, Runtime verification, MCAPL},\n      \tnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n     }\n\n
\n
\n\n\n
\n When applying formal verification to a system that interacts with the real world, we must use a model of the environment. This model represents an abstraction of the actual environment, so it is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well behaved. A solution to this problem consists in exploiting the model of the environment used for statically verifying the system’s behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The article discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies: an autonomous cruise control system and a simulation of the Mars Curiosity rover.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Explaining BDI agent behaviour through dialogue.\n \n \n \n\n\n \n Dennis, L. A.; and Oren, N.\n\n\n \n\n\n\n In 20th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2021), pages 429–437, 2021. \n [RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{DennisAAMAS21,\n      author={Louise A. Dennis and Nir Oren},\n      title={Explaining BDI agent behaviour through dialogue},\n      editors={U.~Endriss and A.~Now\\'{e} and F.~Dignum and A.~Lomuscio},\n      booktitle={20th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2021)},\n      year={2021},\n      pages = {429–437},\n      note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n      }\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Towards a Framework for Certification of Reliable Autonomous Systems.\n \n \n \n\n\n \n Fisher, M.; Mascardi, V.; Rozier, K. Y.; Schlingloff, B.; Winikoff, M.; and Yorke-Smith, N.\n\n\n \n\n\n\n Autonomous Agents and Multi Agent Systems, 35(1): 8. 2021.\n [S4, RAIN, FAIR-Space, ORCA, TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{FisherMRSWY21,\n  author    = {Michael Fisher and\n               Viviana Mascardi and\n               Kristin Yvonne Rozier and\n               Bernd{-}Holger Schlingloff and\n               Michael Winikoff and\n               Neil Yorke{-}Smith},\n  title     = {Towards a Framework for Certification of Reliable Autonomous Systems},\n  journal   = {Autonomous Agents and Multi Agent Systems},\n  volume    = {35},\n  number    = {1},\n  pages     = {8},\n  year      = {2021},\n  doi       = {10.1007/s10458-020-09487-2},\n  note={[<span class="s4">S4</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>,\n        <span class="orca">ORCA</span>, <span class="tas_vn">TAS Verifiability Node</span>]}\n}\n\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (13)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Runtime Verification of the ARIAC competition: Can a robot be Agile and Safe at the same time?.\n \n \n \n\n\n \n Ferrando, A.; Kootbally, Z.; Piliptchak, P.; Cardoso, R. C.; Schlenoff, C.; and Fisher, M.\n\n\n \n\n\n\n In AIRO, 2020. \n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{FerrandoAIRO,\nauthor="Ferrando, Angelo\nand Kootbally, Zeid\nand Piliptchak, Pavel\nand Cardoso, Rafael C.\nand Schlenoff, Craig\nand Fisher, Michael",\ntitle="Runtime Verification of the ARIAC competition: Can a robot be Agile and Safe at the same time?",\nbooktitle="AIRO",\nyear="2020",\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Towards Compositional Verification for Modular Robotic Systems.\n \n \n \n\n\n \n Cardoso, R. C.; Dennis, L. A.; Farrell, M.; Fisher, M.; and Luckcuck, M.\n\n\n \n\n\n\n In Proceedings Second Workshop on Formal Methods for Autonomous Systems, Virtual, 7th of December 2020, volume 329, of Electronic Proceedings in Theoretical Computer Science, pages 15-22, 2020. Open Publishing Association\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{Cardoso20e,\n  author    = {Cardoso, Rafael C. and Dennis, Louise A. and Farrell, Marie and Fisher, Michael and Luckcuck, Matt},\n  year      = {2020},\n  title     = {Towards Compositional Verification for Modular Robotic Systems},\n  booktitle = {Proceedings Second Workshop on\n               Formal Methods for Autonomous Systems,\n               Virtual, 7th of December 2020},\n  series    = {Electronic Proceedings in Theoretical Computer Science},\n  volume    = {329},\n  publisher = {Open Publishing Association},\n  pages     = {15-22},\n  doi       = {10.4204/EPTCS.329.2},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Safety Framework for Critical Systems Utilising Deep Neural Networks.\n \n \n \n\n\n \n Zhao, X.; Banks, A.; Sharp, J.; Robu, V.; Flynn, D.; Fisher, M.; and Huang, X.\n\n\n \n\n\n\n In Proc. 39th International Conference on Computer Safety, Reliability, and Security (SAFECOMP), volume 12234, of Lecture Notes in Computer Science, pages 244–259, 2020. Springer\n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{ZhaoBSRF0020,\n  author    = {Xingyu Zhao and\n               Alec Banks and\n               James Sharp and\n               Valentin Robu and\n               David Flynn and\n               Michael Fisher and\n               Xiaowei Huang},\n  title     = {A Safety Framework for Critical Systems Utilising Deep Neural Networks},\n  booktitle = {Proc. 39th International Conference on Computer Safety, Reliability, and Security (SAFECOMP)},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {12234},\n  pages     = {244--259},\n  publisher = {Springer},\n  year      = 2020,\n  doi       = {10.1007/978-3-030-54549-9_16},\n  note = {[<span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n LFC: Combining Autonomous Agents and Automated Planning in the Multi-Agent Programming Contest.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; and Papacchini, F.\n\n\n \n\n\n\n In The Multi-Agent Programming Contest 2019, pages 31–58, Cham, 2020. Springer International Publishing\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{Cardoso20d,\nauthor="Cardoso, Rafael C.\nand Ferrando, Angelo\nand Papacchini, Fabio",\ntitle="LFC: Combining Autonomous Agents and Automated Planning in the Multi-Agent Programming Contest",\nbooktitle="The Multi-Agent Programming Contest 2019",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="31--58",\nisbn="978-3-030-59299-8",\ndoi={10.1007/978-3-030-59299-8_2},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Ethical Governor Systems viewed as a Multi-Agent Problem.\n \n \n \n \n\n\n \n Cardoso, R. C.; Ene, D.; Evans, T.; and Dennis, L. A.\n\n\n \n\n\n\n In Nallur, V., editor(s), Second Workshop on Implementing Machine Ethics, June 2020. Zenodo\n [RAIN]\n\n\n\n
\n\n\n\n \n \n \"EthicalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{cardosoime,\n  author = {Rafael C. Cardoso and Daniel Ene and Tom Evans and Louise A. Dennis},\n  title = {Ethical Governor Systems viewed as a Multi-Agent Problem},\n  editor       = {Vivek Nallur},\n  booktitle        = {Second Workshop on Implementing Machine Ethics},\n  month        = jun,\n  year         = 2020,\n  publisher    = {Zenodo},\n  doi          = {10.5281/zenodo.3938851},\n  url          = {https://doi.org/10.5281/zenodo.3938851},\n  note = {[<span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Adaptable and Verifiable BDI Reasoning.\n \n \n \n\n\n \n Stringer, P.; Cardoso, R. C.; Huang, X.; and Dennis, L. A.\n\n\n \n\n\n\n In Proceedings of the First Workshop on Agents and Robots for reliable Engineered Autonomy, Virtual event, 4th September 2020, volume 319, of Electronic Proceedings in Theoretical Computer Science, pages 117-125, 2020. Open Publishing Association\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@Inproceedings{Stringer20a,\n  author    = {Stringer, Peter and Cardoso, Rafael C. and Huang, Xiaowei and Dennis, Louise A.},\n  year      = {2020},\n  title     = {Adaptable and Verifiable BDI Reasoning},\n  booktitle = {Proceedings of the First Workshop on\n               Agents and Robots for reliable Engineered Autonomy,\n                Virtual event, 4th September 2020},\n  series    = {Electronic Proceedings in Theoretical Computer Science},\n  volume    = {319},\n  publisher = {Open Publishing Association},\n  pages     = {117-125},\n  doi       = {10.4204/EPTCS.319.9},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verification and Validation for Space Robotics.\n \n \n \n\n\n \n Cardoso, R. C.; Farrell, M.; Kourtis, G.; Webster, M.; Dennis, L. A.; Dixon, C.; Fisher, M.; and Lisitsa, A.\n\n\n \n\n\n\n 2020.\n Poster presented at the Opportunities and Challenges in Space Robotics Workshop held with ICRA 2020. [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@unpublished{Cardoso20c,\n  author    = {Cardoso, R. C. and Farrell, M. and Kourtis, G. and Webster, M. and Dennis, L. A. and Dixon, C. and Fisher, M. and Lisitsa, A.},\n  title     = {Verification and Validation for Space Robotics},\n  year      = {2020},\n  note = {Poster presented at the Opportunities and Challenges in Space Robotics Workshop held with ICRA 2020. [<span class="fs">FAIR-SPACE</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n ROSMonitoring: A Runtime Verification Framework for ROS.\n \n \n \n\n\n \n Ferrando, A.; Cardoso, R. C.; Fisher, M.; Ancona, D.; Franceschini, L.; and Mascardi, V.\n\n\n \n\n\n\n In Towards Autonomous Robotic Systems, pages 387–399, Cham, 2020. Springer International Publishing\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 15 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{Ferrando20a,\nauthor="Ferrando, Angelo\nand Cardoso, Rafael C.\nand Fisher, Michael\nand Ancona, Davide\nand Franceschini, Luca\nand Mascardi, Viviana",\ntitle="ROSMonitoring: A Runtime Verification Framework for ROS",\nbooktitle="Towards Autonomous Robotic Systems",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="387--399",\ndoi="10.1007/978-3-030-63486-5_40",\nisbn="978-3-030-63486-5",\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verifiable Self-Aware Agent-Based Autonomous Systems.\n \n \n \n\n\n \n Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n Proceedings of the IEEE special issue on Self-Aware Autonomous Systems,1011-1026. 2020.\n [Verifiable Autonomy, FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{dennis_ieee20,\n  author={Louise A. Dennis and Michael Fisher},\n  title ={Verifiable Self-Aware Agent-Based Autonomous Systems},\n  journal={Proceedings of the IEEE special issue on Self-Aware Autonomous Systems},\n  pages={1011-1026},\n  doi={10.1109/JPROC.2020.2991262},\n  note = {[<span class="va">Verifiable Autonomy</span>, <span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]},\nyear=2020}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An Interface for Programming Verifiable Autonomous Agents in ROS.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In Bassiliades, N.; Chalkiadakis, G.; and de Jonge, D., editor(s), Multi-Agent Systems and Agreement Technologies, pages 191–205, Cham, 2020. Springer International Publishing\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Cardoso20b,\n  author="Cardoso, Rafael C.\nand Ferrando, Angelo\nand Dennis, Louise A.\nand Fisher, Michael",\neditor="Bassiliades, Nick\nand Chalkiadakis, Georgios\nand de Jonge, Dave",\ntitle="An Interface for Programming Verifiable Autonomous Agents in ROS",\nbooktitle="Multi-Agent Systems and Agreement Technologies",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="191--205",\nabstract="Autonomy has been one of the most desirable features for robotic applications in recent years. This is evidenced by a recent surge of research in autonomous driving cars, strong government funding for research in robotics for extreme environments, and overall progress in service robots. Autonomous decision-making is often at the core of these systems, thus, it is important to be able to verify and validate properties that relate to the correct behaviour that is expected of the system. Our main contribution in this paper, is an interface for integrating BDI-based agents into robotic systems developed using ROS. We use the Gwendolen language to program our BDI agents and to make use of the AJPF model checker in order to verify properties related to the decision-making in the agent programs. Our case studies include 3D simulations using a simple autonomous patrolling behaviour of a TurtleBot, and multiple TurtleBots servicing a house that can cooperate with each other in case of failure.",\nisbn="978-3-030-66412-1",\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n
\n Autonomy has been one of the most desirable features for robotic applications in recent years. This is evidenced by a recent surge of research in autonomous driving cars, strong government funding for research in robotics for extreme environments, and overall progress in service robots. Autonomous decision-making is often at the core of these systems, thus, it is important to be able to verify and validate properties that relate to the correct behaviour that is expected of the system. Our main contribution in this paper, is an interface for integrating BDI-based agents into robotic systems developed using ROS. We use the Gwendolen language to program our BDI agents and to make use of the AJPF model checker in order to verify properties related to the decision-making in the agent programs. Our case studies include 3D simulations using a simple autonomous patrolling behaviour of a TurtleBot, and multiple TurtleBots servicing a house that can cooperate with each other in case of failure.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Heterogeneous Verification of an Autonomous Curiosity Rover.\n \n \n \n\n\n \n Cardoso, R. C.; Farrell, M.; Luckcuck, M.; Ferrando, A.; and Fisher, M.\n\n\n \n\n\n\n In Lee, R.; Jha, S.; Mavridou, A.; and Giannakopoulou, D., editor(s), NASA Formal Methods, pages 353–360, Cham, 2020. Springer International Publishing\n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Cardoso20a,\nauthor="Cardoso, Rafael C.\nand Farrell, Marie\nand Luckcuck, Matt\nand Ferrando, Angelo\nand Fisher, Michael",\neditor="Lee, Ritchie\nand Jha, Susmit\nand Mavridou, Anastasia\nand Giannakopoulou, Dimitra",\ntitle="Heterogeneous Verification of an Autonomous Curiosity Rover",\nbooktitle="NASA Formal Methods",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="353--360",\nabstract="The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy on-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to the communication delays between Earth and Mars. Depending on the orbital position of both planets, it can take 4--24 min for a message to be transmitted between Earth and Mars. If the Curiosity were controlled autonomously, it would be able to perform its activities much faster and more flexibly. However, one of the major barriers to increased use of autonomy in such scenarios is the lack of assurances that the autonomous behaviour will work as expected. In this paper, we use a Robot Operating System (ROS) model of the Curiosity that is simulated in Gazebo and add an autonomous agent that is responsible for high-level decision-making. Then, we use a mixture of formal and non-formal techniques to verify the distinct system components (ROS nodes). This use of heterogeneous verification techniques is essential to provide guarantees about the nodes at different abstraction levels, and allows us to bring together relevant verification evidence to provide overall assurance.",\nisbn="978-3-030-55754-6",\ndoi="10.1007/978-3-030-55754-6_20",\nnote = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n
\n
\n\n\n
\n The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy on-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to the communication delays between Earth and Mars. Depending on the orbital position of both planets, it can take 4–24 min for a message to be transmitted between Earth and Mars. If the Curiosity were controlled autonomously, it would be able to perform its activities much faster and more flexibly. However, one of the major barriers to increased use of autonomy in such scenarios is the lack of assurances that the autonomous behaviour will work as expected. In this paper, we use a Robot Operating System (ROS) model of the Curiosity that is simulated in Gazebo and add an autonomous agent that is responsible for high-level decision-making. Then, we use a mixture of formal and non-formal techniques to verify the distinct system components (ROS nodes). This use of heterogeneous verification techniques is essential to provide guarantees about the nodes at different abstraction levels, and allows us to bring together relevant verification evidence to provide overall assurance.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The ``Why Did You Do That?'' Button: Answering Why-Questions for End Users of Robotic Systems.\n \n \n \n\n\n \n Koeman, V. J.; Dennis, L. A.; Webster, M.; Fisher, M.; and Hindriks, K.\n\n\n \n\n\n\n In Dennis, L. A.; Bordini, R. H.; and Lespérance, Y., editor(s), Engineering Multi-Agent Systems, pages 152–172, Cham, 2020. Springer International Publishing\n [ORCA, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Koeman19EMAS,\nauthor="Koeman, Vincent J.\nand Dennis, Louise A.\nand Webster, Matt\nand Fisher, Michael\nand Hindriks, Koen",\neditor="Dennis, Louise A.\nand Bordini, Rafael H.\nand Lesp{\\'e}rance, Yves",\ntitle="The ``Why Did You Do That?'' Button: Answering Why-Questions for End Users of Robotic Systems",\nbooktitle="Engineering Multi-Agent Systems",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="152--172",\nabstract="The issue of explainability for autonomous systems is becoming increasingly prominent. Several researchers and organisations have advocated the provision of a ``Why did you do that?'' button which allows a user to interrogate a robot about its choices and actions. We take previous work on debugging cognitive agent programs and apply it to the question of supplying explanations to end users in the form of answers to why-questions. These previous approaches are based on the generation of a trace of events in the execution of the program and then answering why-questions using the trace. We implemented this framework in the agent infrastructure layer and, in particular, the Gwendolen programming language it supports -- extending it in the process to handle the generation of applicable plans and multiple intentions. In order to make the answers to why-questions comprehensible to end users we advocate a two step process in which first a representation of an explanation is created and this is subsequently converted into natural language in a way which abstracts away from some events in the trace and employs application specific predicate dictionaries in order to translate the first-order logic presentation of concepts within the cognitive agent program in natural language. A prototype implementation of these ideas is provided.",\nisbn="978-3-030-51417-4",\n  note = {[<span class="orca">ORCA</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n
\n The issue of explainability for autonomous systems is becoming increasingly prominent. Several researchers and organisations have advocated the provision of a ``Why did you do that?'' button which allows a user to interrogate a robot about its choices and actions. We take previous work on debugging cognitive agent programs and apply it to the question of supplying explanations to end users in the form of answers to why-questions. These previous approaches are based on the generation of a trace of events in the execution of the program and then answering why-questions using the trace. We implemented this framework in the agent infrastructure layer and, in particular, the Gwendolen programming language it supports – extending it in the process to handle the generation of applicable plans and multiple intentions. In order to make the answers to why-questions comprehensible to end users we advocate a two step process in which first a representation of an explanation is created and this is subsequently converted into natural language in a way which abstracts away from some events in the trace and employs application specific predicate dictionaries in order to translate the first-order logic presentation of concepts within the cognitive agent program in natural language. A prototype implementation of these ideas is provided.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Plan Library Reconfigurability in BDI Agents.\n \n \n \n\n\n \n Cardoso, R. C.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In Dennis, L. A.; Bordini, R. H.; and Lespérance, Y., editor(s), Engineering Multi-Agent Systems, pages 195–212, Cham, 2020. Springer International Publishing\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Cardoso19EMAS,\nauthor="Cardoso, Rafael C.\nand Dennis, Louise A.\nand Fisher, Michael",\neditor="Dennis, Louise A.\nand Bordini, Rafael H.\nand Lesp{\\'e}rance, Yves",\ntitle="Plan Library Reconfigurability in BDI Agents",\nbooktitle="Engineering Multi-Agent Systems",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="195--212",\nabstract="One of the major advantages of modular architectures in robotic systems is the ability to add or replace nodes, without needing to rearrange the whole system. In this type of system, autonomous agents can aid in the decision making and high-level control of the robot. For example, a robot may have a module for each of the effectors and sensors that it has and an agent with a plan library containing high-level plans to aid in the decision making within these modules. However, when autonomously replacing a node it can be difficult to reconfigure plans in the agent's plan library while retaining correctness. In this paper, we exploit the formal concept of capabilities in Belief-Desire-Intention agents and describe how agents can reason about these capabilities in order to reconfigure their plan library while retaining overall correctness constraints. To validate our approach, we show the implementation of our framework and an experiment using a practical example in the Mars rover scenario.",\nisbn="978-3-030-51417-4",\ndoi="10.1007/978-3-030-51417-4_10",\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n
\n One of the major advantages of modular architectures in robotic systems is the ability to add or replace nodes, without needing to rearrange the whole system. In this type of system, autonomous agents can aid in the decision making and high-level control of the robot. For example, a robot may have a module for each of the effectors and sensors that it has and an agent with a plan library containing high-level plans to aid in the decision making within these modules. However, when autonomously replacing a node it can be difficult to reconfigure plans in the agent's plan library while retaining correctness. In this paper, we exploit the formal concept of capabilities in Belief-Desire-Intention agents and describe how agents can reason about these capabilities in order to reconfigure their plan library while retaining overall correctness constraints. To validate our approach, we show the implementation of our framework and an experiment using a practical example in the Mars rover scenario.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Modular Verification of Autonomous Space Robotics.\n \n \n \n\n\n \n Farrell, M.; Cardoso, R. C.; Dennis, L.; Dixon, C.; Fisher, M.; Kourtis, G.; Lisitsa, A.; Luckcuck, M.; and Webster, M\n\n\n \n\n\n\n In Assurance of Autonomy for Robotic Space Missions Workshop, 2019. \n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Farrell2019b,\n  author    = {Farrell, M. and Cardoso, R. C. and Dennis, L. and Dixon, C. and Fisher, M. and Kourtis, G. and Lisitsa, A. and Luckcuck, M. and Webster, M},\n  title     = {Modular Verification of Autonomous Space Robotics},\n  booktitle = {Assurance of Autonomy for Robotic Space Missions Workshop},\n  year      = {2019},\n  note = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages.\n \n \n \n\n\n \n Farrell, M.; Bradbury, M.; Fisher, M.; Dennis, L. A.; Dixon, C.; Yuan, H.; and Maple, C.\n\n\n \n\n\n\n In Ölveczky, P. C.; and Salaün, G., editor(s), Software Engineering and Formal Methods, pages 471–490, Cham, 2019. Springer International Publishing\n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{Farrell2019,\nauthor="Farrell, Marie\nand Bradbury, Matthew\nand Fisher, Michael\nand Dennis, Louise A.\nand Dixon, Clare\nand Yuan, Hu\nand Maple, Carsten",\neditor="{\\"O}lveczky, Peter Csaba\nand Sala{\\"u}n, Gwen",\ntitle="Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages",\nbooktitle="Software Engineering and Formal Methods",\nyear="2019",\npublisher="Springer International Publishing",\naddress="Cham",\npages="471--490",\nabstract="Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety-and security-critical, since a breach in system security may impact safety. Generally, safety and security concerns for such systems are treated separately during the development process. In this paper, we consider an algorithm for sending Cooperative Awareness Messages (CAMs) between vehicles in a CAV system and the use of CAMs in preventing vehicle collisions. We employ threat analysis techniques that are commonly used in the cyber security domain to guide our formal verification. This allows us to focus our formal methods on those security properties that are particularly important and to consider both safety and security in tandem. Our analysis centres on identifying STRIDE security properties and we illustrate how these can be formalised, and subsequently verified, using a combination of formal tools for distinct aspects, namely Promela/SPIN and Dafny.",\nisbn="978-3-030-30446-1",\nnote = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n
\n
\n\n\n
\n Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety-and security-critical, since a breach in system security may impact safety. Generally, safety and security concerns for such systems are treated separately during the development process. In this paper, we consider an algorithm for sending Cooperative Awareness Messages (CAMs) between vehicles in a CAV system and the use of CAMs in preventing vehicle collisions. We employ threat analysis techniques that are commonly used in the cyber security domain to guide our formal verification. This allows us to focus our formal methods on those security properties that are particularly important and to consider both safety and security in tandem. Our analysis centres on identifying STRIDE security properties and we illustrate how these can be formalised, and subsequently verified, using a combination of formal tools for distinct aspects, namely Promela/SPIN and Dafny.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Summary of Formal Specification and Verification of Autonomous Robotic Systems.\n \n \n \n\n\n \n Luckcuck, M.; Farrell, M.; Dennis, L. A.; Dixon, C.; and Fisher, M.\n\n\n \n\n\n\n In Ahrendt, W.; and Tapia Tarifa, S. L., editor(s), Integrated Formal Methods, pages 538–541, Cham, 2019. Springer International Publishing\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{Luckcuck2019Summary,\nauthor="Luckcuck, Matt and Farrell, Marie and Dennis, Louise A. and Dixon, Clare and Fisher, Michael",\neditor="Ahrendt, Wolfgang and Tapia Tarifa, Silvia Lizeth",\ntitle="A Summary of Formal Specification and Verification of Autonomous Robotic Systems",\nbooktitle="Integrated Formal Methods",\nyear="2019",\npublisher="Springer International Publishing",\naddress="Cham",\ndoi = {10.1007/978-3-030-34968-4_33},\npages="538--541",\nabstract="Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics have received some attention in the literature, but no resource provides a current overview. This short paper summarises the contributions published in [5], which surveys the state-of-the-art in formal specification and verification for autonomous robotics.",\nisbn="978-3-030-34968-4",\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n
\n Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics have received some attention in the literature, but no resource provides a current overview. This short paper summarises the contributions published in [5], which surveys the state-of-the-art in formal specification and verification for autonomous robotics.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Specification and Verification of Autonomous Robotic Systems: A Survey.\n \n \n \n \n\n\n \n Luckcuck, M.; Farrell, M.; Dennis, L. A.; Dixon, C.; and Fisher, M.\n\n\n \n\n\n\n ACM Comput. Surv., 52(5): 1–41. sep 2019.\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{Luckcuck2019,\ntitle = {{Formal Specification and Verification of Autonomous Robotic Systems: A Survey}},\nauthor = {Luckcuck, Matt and Farrell, Marie and Dennis, Louise A. and Dixon, Clare and Fisher, Michael},\ndoi = {10.1145/3342355},\neprint = {1807.00048},\nissn = {03600300},\njournal = {ACM Comput. Surv.},\nmonth = {sep},\nnumber = {5},\npages = {1--41},\nurl = {https://arxiv.org/abs/1807.00048 http://dl.acm.org/citation.cfm?doid=3362097.3342355},\nvolume = {52},\nyear = {2019},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Probabilistic Model Checking of Robots Deployed in Extreme Environments.\n \n \n \n \n\n\n \n Zhao, X.; Robu, V.; Flynn, D.; Dinmohammadi, F.; Fisher, M.; and Webster, M.\n\n\n \n\n\n\n In Proc. 23rd AAAI Conference on Artificial Intelligence, pages 8066–8074, 2019. AAAI Press\n [ORCA]\n\n\n\n
\n\n\n\n \n \n \"ProbabilisticPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{ZhaoRFD0W19,\n  author    = {Xingyu Zhao and\n               Valentin Robu and\n               David Flynn and\n               Fateme Dinmohammadi and\n               Michael Fisher and\n               Matt Webster},\n  title     = {Probabilistic Model Checking of Robots Deployed in Extreme Environments},\n  booktitle = {Proc. 23rd {AAAI} Conference on Artificial Intelligence},\n  pages     = {8066--8074},\n  year      = {2019},\n  publisher = {{AAAI} Press},\n  url       = {https://www.aaai.org/Library/AAAI/aaai19contents.php},\n  note = {[<span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On Enactability of Agent Interaction Protocols: Towards a Unified Approach.\n \n \n \n\n\n \n Ferrando, A.; Winikoff, M.; Cranefield, S.; Dignum, F.; and Mascardi, V.\n\n\n \n\n\n\n In Proc. of the 7th International Workshop on Engineering Multi-Agent Systems (EMAS), 2019. \n [ORCA, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Ferrando19EMAS,\n  author    = {Angelo Ferrando and Michael Winikoff and Stephen Cranefield and Frank Dignum and Viviana Mascardi},\n  title     = {On Enactability of Agent Interaction Protocols: Towards a Unified Approach},\n  booktitle = {Proc. of the 7th International Workshop on Engineering Multi-Agent Systems (EMAS)},\n  year      = {2019},\n  note = {[<span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Decentralised Planning for Multi-Agent Programming Platforms.\n \n \n \n\n\n \n Cardoso, R. C.; and Bordini, R. H.\n\n\n \n\n\n\n In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, of AAMAS '19, pages 799–807, Richland, SC, 2019. International Foundation for Autonomous Agents and Multiagent Systems\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@inproceedings{Cardoso19AAMAS,\nauthor = {Cardoso, Rafael C. and Bordini, Rafael H.},\ntitle = {Decentralised Planning for Multi-Agent Programming Platforms},\nyear = {2019},\nisbn = {9781450363099},\npublisher = {International Foundation for Autonomous Agents and Multiagent Systems},\naddress = {Richland, SC},\nbooktitle = {Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems},\npages = {799–807},\nnumpages = {9},\nkeywords = {multi-agent development platforms, multi-agent planning, hierarchical task network, goal allocation},\nlocation = {Montreal QC, Canada},\nseries = {AAMAS '19},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Slicing Agent Programs for more Efficient Verification.\n \n \n \n\n\n \n Winikoff, M.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In Weyns, D.; Mascardi, V.; and Ricci, A., editor(s), Proc. 6th International Workshop in Engineering Multi-Agent Systems, volume 11375, of Lecture Notes in Computer Science, pages 139-157, Stockholm, Sweden, 2019. \n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{WinikoffDF:EMAS18,\n   author = {Michael Winikoff and Louise A. Dennis and Michael Fisher},\n   title = "{Slicing Agent Programs for more Efficient Verification}",\nbooktitle = {Proc. 6th International Workshop in Engineering Multi-Agent Systems},\nyear = {2019},\nvolume={11375},\npages={139-157},\neditor={D. Weyns and V. Mascardi and A. Ricci},\nseries={Lecture Notes in Computer Science},\naddress = {Stockholm, Sweden},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (12)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Verifiable Self-Certifying Autonomous Systems.\n \n \n \n\n\n \n Fisher, M.; Collins, E.; Dennis, L. A.; Luckcuck, M.; Webster, M.; Jump, M.; Page, V.; Patchett, C.; Dinmohammadi, F.; Flynn, D.; Robu, V.; and Zhao, X.\n\n\n \n\n\n\n In 2018 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pages 341-348, Oct 2018. \n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{8539217,\n  author    = {Michael Fisher and Emily Collins and Louise A. Dennis and Matt Luckcuck and Matthew Webster and Michael Jump and Vincent Page and Charles Patchett and Fateme Dinmohammadi\n            and David Flynn and Valentin Robu and Xingu Zhao},\n  title     = {Verifiable Self-Certifying Autonomous Systems},\n  booktitle = {2018 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)},\n  year      = {2018},\n  pages     = {341-348},\n  month     = {Oct},\n  doi       = {10.1109/ISSREW.2018.00028},\n  note = {[<span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments.\n \n \n \n\n\n \n Nalon, C.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n In 2018. Springer\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{NalonHD18,\nauthor = {Cl\\'audia Nalon and Ullrich Hustadt and Clare Dixon},\ntitle = "{KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments}",\njournal = {Journal of Automated Reasoning},\nyear = {2018},\n  volume    = {},\npublisher = {Springer},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks.\n \n \n \n\n\n \n Webster, M.; Breza, M.; Dixon, C.; Fisher, M.; and McCann, J.\n\n\n \n\n\n\n Electronic Communications of the EASST. 2018.\n [FAIR-SPACE, ORCA, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{WebsterBDFM18,\n  author    =  {Matthew Webster and Michael Breza and Clare Dixon and Michael Fisher and Julie McCann},\n  title     = {Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks},\n  journal   = {Electronic Communications of the EASST},\n  volume    = {},\n  year      = {2018},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics.\n \n \n \n \n\n\n \n Hustadt, U.; Nalon, C.; and Dixon, C.\n\n\n \n\n\n\n In Konev, B.; Urban, J.; and Rümmer, P., editor(s), Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR), of CEUR Workshop Proceedings, pages 34–48, Aachen, 2018. \n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n \n \"EvaluatingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{HustadtEtAl:PAAR2018,\nauthor = {Ullrich Hustadt and Cl\\'audia Nalon and Clare Dixon},\ntitle = "{Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics}",\nbooktitle = {Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR)},\nyear = {2018},\npages = {34--48},\neditor = {Boris Konev and Josef Urban and Philipp R\\"ummer},\nnumber = 2162,\nseries = {CEUR Workshop Proceedings},\naddress = {Aachen},\nissn = {1613-0073},\nurl = {http://ceur-ws.org/Vol-2162/#paper-04},\nvenue = {Oxford, UK},\neventdate = {2018-07-19},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Machines That Know Right And Cannot Do Wrong: The Theory and Practice of Machine Ethics.\n \n \n \n \n\n\n \n Dennis, L. A.; and Slavkovik, M.\n\n\n \n\n\n\n IEEE Intelligent Informatics Bulletin, 19(1). 2018.\n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"MachinesPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{dennis18iib,\n  author = {Louise A. Dennis and Marija Slavkovik},\n  title = {Machines That Know Right And Cannot Do Wrong: The Theory and Practice of Machine Ethics},\n  journal = {IEEE Intelligent Informatics Bulletin},\n  volume = 19,\n  number = 1,\n  year = 2018,\n  url = {http://www.comp.hkbu.edu.hk/~cib/2018/Aug/article2/iib_vol19no1_article2.pdf},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verifying and Validating Autonomous Systems: an Integrated Approach.\n \n \n \n\n\n \n Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; and Mascardi, V.\n\n\n \n\n\n\n In Proc. 8th IEEE International Conference on Runtime Verification (RV), 2018. \n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{Ferrando:RV18,\n   author = {Angelo Ferrando and Louise A. Dennis and Davide Ancona and Michael Fisher and Viviana Mascardi},\n    title = "{Verifying and Validating Autonomous Systems: an Integrated Approach}",\nbooktitle = {Proc. 8th IEEE International Conference on Runtime\n                  Verification (RV)},\nyear = {2018},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Robotics and Integrated Formal Methods: Necessity Meets Opportunity.\n \n \n \n \n\n\n \n Farrell, M.; Luckcuck, M.; and Fisher, M.\n\n\n \n\n\n\n In Furia, C. A.; and Winter, K., editor(s), Proc. 14th International Conference on Integrated Formal Methods (iFM), volume 11023, of Lecture Notes in Computer Science, pages 161-171, 2018. Springer\n [FAIR-SPACE, ORCA, RAIN]\n\n\n\n
\n\n\n\n \n \n \"RoboticsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{FarrellLF:IFM018,\n  author    = {Marie Farrell and Matt Luckcuck and Michael Fisher},\n  editor    = {Carlo A. Furia and Kirsten Winter},\n  title     = {Robotics and Integrated Formal Methods: Necessity Meets Opportunity},\n  booktitle = {Proc. 14th International Conference on Integrated\n               Formal Methods (iFM)},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {11023},\n  pages     = {161-171},\n  publisher = {Springer},\n  year      = {2018},\n  url       = {https://doi.org/10.1007/978-3-319-98938-9_10},\n  doi       = {10.1007/978-3-319-98938-9_10},\n  biburl    = {https://dblp.org/rec/bib/conf/ifm/FarrellL018},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Clarification of Ambiguity for the Simple Authentication and Security Layer.\n \n \n \n \n\n\n \n Al-Shareefi, F.; Lisitsa, A.; and Dixon, C.\n\n\n \n\n\n\n In Butler, M. J.; Raschke, A.; Hoang, T. S.; and Reichl, K., editor(s), Proc. 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ), volume 10817, of Lecture Notes in Computer Science, pages 189-203, 2018. Springer\n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n \n \"ClarificationPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{AlShareefiLD:ABZ18,\n  author    = {Farah Al{-}Shareefi and\n               Alexei Lisitsa and Clare Dixon},\n  editor    = {Michael J. Butler and\n               Alexander Raschke and\n               Thai Son Hoang and\n               Klaus Reichl},\n  title     = "{Clarification of Ambiguity for the Simple Authentication\n                and Security  Layer}",\n  booktitle = {Proc. 6th International Conference on Abstract\n               State Machines, Alloy, B, TLA, VDM, and {Z} (ABZ)},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {10817},\n  pages     = {189-203},\n  publisher = {Springer},\n  year      = {2018},\n  url       = {https://doi.org/10.1007/978-3-319-91271-4\\_13},\n  doi       = {10.1007/978-3-319-91271-4\\_13},\n  biburl    = {https://dblp.org/rec/bib/conf/asm/Al-ShareefiLD18},\n  note = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verifiable Self-Certifying Autonomous Systems.\n \n \n \n\n\n \n Fisher, M.; Collins, E.; Dennis, L. A.; Luckcuck, M.; Webster, M.; Jump, M.; Page, V.; Patchett, C.; Dinmohammadi, F.; Flynn, D.; Robu, V.; and Zhao, X.\n\n\n \n\n\n\n In Proc. 8th IEEE International Workshop on Software Certification (WoSoCer), Memphis, USA, 2018. \n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{Fisher:WoSoCer18,\n   author = {Michael Fisher and Emily Collins and Louise A. Dennis and Matt Luckcuck and Matthew Webster and Michael Jump and Vincent Page and Charles Patchett and Fateme Dinmohammadi\n            and David Flynn and Valentin Robu and Xingu Zhao},\n    title = "{Verifiable Self-Certifying Autonomous Systems}",\nbooktitle = {Proc. 8th IEEE International Workshop on Software Certification (WoSoCer)},\nyear = {2018},\naddress = {Memphis, USA},\nnote = {[<span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Certification of Safe and Trusted Robotic Inspection of Assets.\n \n \n \n\n\n \n Dinmohammadi, F.; Flynn, D.; Fisher, M.; Jump, M.; Page, V.; Robu, V.; Patchett, C.; Tang, W.; and Webster, M.\n\n\n \n\n\n\n In Proc. Prognostics and System Health Management Conference (PHM-Chongqing), Chongqing, China, 2018. IEEE\n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@INPROCEEDINGS{Dinmohammadi:PHM18,\nauthor={Fateme Dinmohammadi and David Flynn and Michael Fisher and Michael Jump and Vincent Page and Valentin Robu and Charles Patchett and Wenshuo Tang and Matthew Webster},\nbooktitle={Proc. Prognostics and System Health Management\n     Conference (PHM-Chongqing)},\ntitle="{Certification of Safe and Trusted Robotic Inspection of Assets}",\nyear={2018},\nvolume={},\nnumber={},\naddress = {Chongqing, China},\npages={},\npublisher = {IEEE},\nnote = {[<span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Recognising Assumption Violations in Autonomous Systems Verification.\n \n \n \n \n\n\n \n Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; and Mascardi, V.\n\n\n \n\n\n\n In Proc. 17th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS), pages 1933–1935, 2018. IFAAMAS/ACM\n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"RecognisingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{FerrandoDA0M18,\n  author    = {Angelo Ferrando and Louise A. Dennis and Davide Ancona and Michael Fisher and Viviana Mascardi},\n  title     = "{Recognising Assumption Violations in Autonomous Systems Verification}",\n  booktitle = {Proc. 17th International Conference on Autonomous Agents\n               and MultiAgent Systems (AAMAS)},\n  pages     = {1933--1935},\n  year      = {2018},\n  publisher = {IFAAMAS/ACM},\n  url       = {http://dl.acm.org/citation.cfm?id=3238028},\n  timestamp = {Mon, 16 Jul 2018 09:21:17 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/atal/FerrandoDA0M18},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Modular Verification of Vehicle Platooning with Respect to Decisions, Space and Time.\n \n \n \n \n\n\n \n Kamali, M.; Linker, S.; and Fisher, M.\n\n\n \n\n\n\n In Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), 2018. \n [FAIR-SPACE,S4,Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"ModularPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{KamaliLF:FTSCS18,\n  author    = {Maryam Kamali and Sven Linker and Michael Fisher},\n  title     = "{Modular Verification of Vehicle Platooning with Respect to Decisions,\n               Space and Time}",\n  booktitle = {Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)},\n  year      = {2018},\n  url       = {http://arxiv.org/abs/1804.06647},\n  note = {[<span class="fs">FAIR-SPACE</span>,<span class="s4">S4</span>,<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);